es:ES, e:E, l:IdLnk, tg:Id.
kind(e) = rcv(l,tg)  Knd  {loc(e) = destination(l)  Id & loc(sender(e)) = source(l)  Id} 

latex

Definitions	ES, t  T, x:A. B(x), E, IdLnk, Id, rcv(l,tg), kind(e), Knd, Prop, {T}, P  Q, isrcv(e), b, True, isrcv(k), SQType(T), source(l), sender(e), loc(e), P  Q, Dec(P), destination(l), P & Q, lnk(k), lnk(e), sends(l;e), ||as||, (Msg on l)
Lemmas	length wf1, es-Msgl wf, es-index wf, es-axioms, ldst wf, decidable equal Id, es-loc wf, es-sender wf, lsrc wf, Knd sq, Knd wf, es-kind wf, rcv wf, Id wf, IdLnk wf, es-E wf, event system wf